r:rationals. qrep(r)  (:  int_nzero) 

latex

Definitions

gt(i; j), P  Q, T, True, P  Q, P  Q, x:A. B(x), A c B, divides(b; a), gcd_p(a; b; y), coprime(a; b), prop{i:l}, guard(T), sq_type(T), P  Q, spreadn(a; x,y,z.t(x;y;z)), False, P  Q, A, nequal(T; a; b), int_nzero, top, ff, if b then t else f fi , tt, qrep(r), t  T, x:A. B(x), decidable(P), Unit, A  B, , qeq(r; s), , b-union(A; B), rationals,

Lemmas

decidable lt, decidable int equal, pos mul arg bounds, assoced weakening, divides functionality wrt assoced, assoced elim, neg mul arg bounds, assert of lt int, bnot of le int, true wf, squash wf, eqff to assert, assert of le int, iff transitivity, bnot wf, lt int wf, coprime-equiv-unique-pair, le wf, assert wf, le int wf, one divs any, coprime wf, mul cancel in eq, nat wf, gcd reduce wf, gcd reduce property, nequal wf, rationals wf, assert of eq int, eqtt to assert, isint-int, int nzero wf, btrue wf, qeq wf, bool wf